/**
 * Copyright (c) 2010 CWI Amsterdam and others. All rights reserved.
 * This program and the accompanying materials are made available
 * under the terms of the Eclipse Public License v1.0
 * which accompanies this distribution, and is available at
 * http://www.eclipse.org/legal/epl-v10.html
 * 
 * Contributors:
 *    CWI Amsterdam - initial API and implementation
 */
package nl.cwi.arne.ui.jobs;

import java.io.File;
import java.io.IOException;

import nl.cwi.arne.NetworkActivation;
import nl.cwi.arne.lts.LTS;
import nl.cwi.arne.lts.resource.LTSResource;
import nl.cwi.arne.mcrl2.Specification;
import nl.cwi.arne.mcrl2.toolchains.GenerateLTSToolChain;
import nl.cwi.arne.mcrl2.toolchains.ShowLTSToolChain;
import nl.cwi.arne.ui.ArnePreferences;
import nl.cwi.arne.ui.ArneUIPlugin;

import org.eclipse.core.runtime.IProgressMonitor;
import org.eclipse.core.runtime.IStatus;
import org.eclipse.core.runtime.Status;
import org.eclipse.emf.common.util.URI;

/**
 * @author Christian Krause
 */
public class ShowLTSJob extends AbstractArneUIJob {
	
	// Activation to be displayed:
	private NetworkActivation activation;
	
	/**
	 * Default constructor.
	 * @param activation Activation.
	 */
	public ShowLTSJob(NetworkActivation activation) {
		super("Showing LTS...");
		this.activation = activation;
	}

	/* (non-Javadoc)
	 * @see org.eclipse.core.runtime.jobs.Job#run(org.eclipse.core.runtime.IProgressMonitor)
	 */
	@Override
	protected IStatus run(IProgressMonitor monitor) {
				
		// Generate a mCRL2 specification:
		Specification spec = getInitializedTranslator().generateSpecification(activation);
		printlnToMCRL2Console(spec);
		
		// Generate the LTS:
		GenerateLTSToolChain toolchain = new GenerateLTSToolChain(spec, ArnePreferences.getMCRL2Options());
		toolchain.setCaptureOutput(true);
		IStatus status = toolchain.execute(monitor);
		if (status.getSeverity()!=IStatus.OK) {
			return status;
		}
		toolchain.getLPSFile().delete();
		File file = toolchain.getLTSFile();
		
		// Remove initial state if required:
		if (activation.getNetwork().hasUnknownStartLevels() && 
			ArnePreferences.isRemoveInitialStates()) {
			
			try {
				LTSResource resource = new LTSResource(URI.createFileURI(file.getAbsolutePath()));
				resource.load(null);
				LTS lts = resource.getLTS();
				lts.removeState(lts.getInitialState());
				lts.setInitialState(lts.getStates().get(0));
				resource.save(null);
			} catch (IOException e) {
				return new Status(IStatus.ERROR, ArneUIPlugin.PLUGIN_ID, 0, "Error loading LTS", e);
			}
		}
		
		// Show the LTS:
		toolchain = new ShowLTSToolChain(file, ArnePreferences.getMCRL2Options());
		return toolchain.execute(monitor);
		
	}

}
